#ifndef PDT_Z3_GRAPHVISITOR_H
#define PDT_Z3_GRAPHVISITOR_H

#include "PDTGraphVisitor.h"

#include <vector>
#include <map>
#include <stack>
#include <sstream>
using namespace std;

//added because of circular includes
class PDTNode;
class PDTCodeGraph;

class PDTSMT2Visitor : public PDTGraphVisitor
{
private:

public:
  const char ** arrStatement;
  const char ** inGamma;
  const char ** eOrd;
  const char ** s2i;

  unsigned int counter; // TODO: number of nodes traversed so far
  unsigned int boundCounter;
  stringstream ss;

  PDTNode * currentNode;
  PDTCodeGraph & cg;

  PDTSMT2Visitor(PDTCodeGraph & aCG);
  virtual ~ PDTSMT2Visitor();


  void defineArraysOfStatements();

  typedef enum {
      Unsat, Sat, None
  } Sat_Em;
  Sat_Em check() ;


  virtual bool pre(PDTNode*){return true;}
  virtual bool in(PDTNode*, PDTNode*, unsigned int){return true;}
  virtual bool post(PDTNode*){return true;}

  static const char * Z3Params;
  static const char * declarations; 
};

#endif // PDT_Z3_GRAPHVISITOR_H
